Conversation
The IOAPIC polarity for an interrupt pin is 0=High and 1=Low based on how the tool eventually makes the kernel system call, which casts the enum value to a word and then passes it to the kernel. The kernel then ors in the value passed at the corresponding bit position in the ioredtbl_state. Signed-off-by: Callum <c.berry@student.unsw.edu.au>
|
I don't think it makes sense to add breaking changes for something that in the end is arbitrary, and is (hopefully) documented correctly. If anything (I seem to recall discussing polarity with @dreamliner787-9 at some point) it makes more sense to use a string, as in "polarity=high" or "polarity=rising" or combine them as "trigger=level_high" or some such). |
|
I don't think the current behaviour is really arbitrary, it's my understanding that atm if you write in the SDF "low" the kernel will in the end configure the polarity as high and vice-versa... |
|
@cazb2 I think you are right but when making a PR like this you should point to the actual kernel source code or documentation that backs up your argument. When I checked the manual it didn't make it clear what argument values relate to what actual polarity, so please point to source code and explain why the Microkit tool is doing the wrong thing. |
|
Yep nws I can update my description. |
3 participants
The kernel syscall for configuring ioapic pins bitwise or's the polarity value passed in the syscall. If a user wants a low polarity pin they pass the value 1, and if a user wants a high polarity pin they pass 0.
https://github.com/seL4/seL4/blob/82a1a8f48f3d16fecb5398be9200007d59675ff9/src/plat/pc99/machine/ioapic.c#L190-L194
Currently the microkit tool does the opposite i.e. passing 0 for a low polarity configuration and passing 1 for a high polarity configuration. The enum definition is what this code changes. The value is actually used here:
microkit/tool/microkit/src/capdl/irq.rs
Lines 73 to 87 in cbc4c9d